Nuprl Lemma : fpf-ap_functionality
11,40
postcript
pdf
eq1
,
eq2
,
f
,
x
:top. sqequal(fpf-ap(
f
;
eq2
;
x
); fpf-ap(
f
;
eq1
;
x
))
latex
Definitions
x
:
A
.
B
(
x
)
,
fpf-ap(
f
;
eq
;
x
)
,
t
T
Lemmas
top
wf
origin
eq1,eq2,f,x:top. sqequal(fpf-ap(f; eq2; x); fpf-ap(f; eq1; x)) eq1,eq2,f,x:top. sqequal(fpf-ap(f; eq2; x); fpf-ap(f; eq1; x)) x:A. B(x)
T